CNR Author
operator:
and / or
Typology
operator:
and / or
Language
operator:
and / or
Date
operator:
and / or
Rights
operator:
and / or
2023
Software
Unknown
A toolchain for strategy synthesis with spatial properties - Complementary material
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
Basile D., Ter Beek M. H., Bussi L., Ciancia V.
This is the complementary material for our paper ``A Toolchain for Strategy Synthesis with Spatial Properties'' accepted for publication at the Journal of Software Tools and Technology Transfer. This repository contains a permanent snapshot of https://github.com/contractautomataproject/CATLib_PngConverter/tree/ec0938043146b008bbbcb4ed3ec79c06dd2e47d6DOI: 10.5281/zenodo.8220527
Metrics:
See at: CNR ExploRA
2023
Journal article
Open Access
A toolchain for strategy synthesis with spatial properties
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
Basile D., Ter Beek M. H, Bussi L., Ciancia V.
We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools \texttt{CATLib} and \texttt{VoxLogicA} to interact in a fully automated way. The Contract Automata Library (\texttt{CATLib}) is aimed at both composition and strategy synthesis of games modelled in a dialect of finite state automata. The Voxel-based Logical Analyser (\texttt{VoxLogicA}) is a spatial model checker for the verification of properties expressed using the Spatial Logic of Closure Spaces on pixels of digital images. We provide examples of strategy synthesis on automata encoding motion of agents in spaces represented by images, as well as a proof-of-concept realistic example based on a case study from the railway domain. The strategies are synthesised with \texttt{CAT\-Lib}, while the properties to enforce are defined by means of spatial model checking of the images with \texttt{VoxLogicA}. The combination of spatial model checking with strategy synthesis provides a toolchain for checking and enforcing mobility properties in multi-agent systems in which location plays an important role, like in many collective adaptive systems. We discuss the toolchain's performance also considering several recent improvements.Source: International journal on software tools for technology transfer (Print) 25 (2023): 641–658. doi:10.1007/s10009-023-00730-1
DOI: 10.1007/s10009-023-00730-1
Metrics:
See at:
ISTI Repository 
| ISTI Repository | CNR ExploRA
2022
Contribution to book
Open Access
Towards model checking video streams using VoxLogicA on GPUs
Bussi L., Ciancia V., Gadducci F., Latella D., Massink M.
We present a feasibility study on the use of spatial logic model checking for real-time analysis of high-resolution video streams with the tool VoxLogicA. VoxLogicA is a voxel-based image analyser based on the Spatial Logic for Closure Spaces, a logic catered to deal with properties of spatial structures such as topological spaces, graphs and polyhedra. The underlying language includes operators to model proximity and reachability. We demonstrate, via the analysis of a series of video frames from a well-known video game, that it is possible to analyse high-resolution videos in real-time by exploiting the speed-up of VoxLogicA-GPU, a recently developed GPU-based version of the tool, which is 1-2 orders of magnitude faster than its previous iteration. Potential applications of real-time video analysis include medical imaging applications such as ultrasound exams, and other video-based diagnostic techniques. More broadly speaking, this work can be the first step towards novel information retrieval methods suitable to find information in a declarative way, in possibly large collections of video streams.Source: From Data to Models and Back, edited by Bowles J., Broccia G., Pellungrini R., pp. 78–90, 2022
DOI: 10.1007/978-3-031-16011-0_6
Metrics:
Bussi L., Ciancia V., Gadducci F., Latella D., Massink M.
We present a feasibility study on the use of spatial logic model checking for real-time analysis of high-resolution video streams with the tool VoxLogicA. VoxLogicA is a voxel-based image analyser based on the Spatial Logic for Closure Spaces, a logic catered to deal with properties of spatial structures such as topological spaces, graphs and polyhedra. The underlying language includes operators to model proximity and reachability. We demonstrate, via the analysis of a series of video frames from a well-known video game, that it is possible to analyse high-resolution videos in real-time by exploiting the speed-up of VoxLogicA-GPU, a recently developed GPU-based version of the tool, which is 1-2 orders of magnitude faster than its previous iteration. Potential applications of real-time video analysis include medical imaging applications such as ultrasound exams, and other video-based diagnostic techniques. More broadly speaking, this work can be the first step towards novel information retrieval methods suitable to find information in a declarative way, in possibly large collections of video streams.Source: From Data to Models and Back, edited by Bowles J., Broccia G., Pellungrini R., pp. 78–90, 2022
DOI: 10.1007/978-3-031-16011-0_6
Metrics:
See at:
ISTI Repository | link.springer.com 
| CNR ExploRA
2022
Conference article
Closed Access
On binding in the spatial logics for closure spaces
Bussi L., Ciancia V., Gadducci F., Latella D., Massink M.
We present two different extensions of the spatial logic for closure spaces (SLCS), and its spatio-temporal variant (?SLCS), with spa- tial quantification operators. The first concerns the existential quantifi- cation on individual points of a space. The second concerns the quantifi- cation on sets of points. The latter amounts to a form of quantification over atomic propositions, thus without the full power of second order logic. The spatial quantification operators are useful for reasoning about the existence of particular spatial objects in a space, their spatial rela- tion with respect to other spatial objects, and, in the spatio-temporal setting, to reason about the dynamic evolution of such spatial objects in time and space, including reasoning about newly introduced items. In this preliminary study we illustrate the expressiveness of the operators by means of several small, but representative, examples.Source: ISoLA 2022 - 11th International Symposium, pp. 479–497, Rhodes, Greece, 22-30/10/2022
DOI: 10.1007/978-3-031-19849-6_27
Metrics:
Bussi L., Ciancia V., Gadducci F., Latella D., Massink M.
We present two different extensions of the spatial logic for closure spaces (SLCS), and its spatio-temporal variant (?SLCS), with spa- tial quantification operators. The first concerns the existential quantifi- cation on individual points of a space. The second concerns the quantifi- cation on sets of points. The latter amounts to a form of quantification over atomic propositions, thus without the full power of second order logic. The spatial quantification operators are useful for reasoning about the existence of particular spatial objects in a space, their spatial rela- tion with respect to other spatial objects, and, in the spatio-temporal setting, to reason about the dynamic evolution of such spatial objects in time and space, including reasoning about newly introduced items. In this preliminary study we illustrate the expressiveness of the operators by means of several small, but representative, examples.Source: ISoLA 2022 - 11th International Symposium, pp. 479–497, Rhodes, Greece, 22-30/10/2022
DOI: 10.1007/978-3-031-19849-6_27
Metrics:
See at:
link.springer.com | CNR ExploRA
2021
Conference article
Open Access
Querying medical imaging datasets using spatial logics (Position paper)
Belmonte G., Broccia G., Bussi L., Ciancia V., Latella D., Massink M.
Nowadays a plethora of health data is available for clinical and research usage. Such existing datasets can be augmented through artificial-intelligence-based methods by automatic, personalised annotations and recommendations. This huge amount of data lends itself to new usage scenarios outside the boundaries where it was created; just to give some examples: to aggregate data sources in order to make research work more relevant; to incorporate a diversity of datasets in training of Machine Learning algorithms; to support expert decisions in telemedicine. In such a context, there is a growing need for a paradigm shift towards means to interrogate medical databases in a semantically meaningful way, fulfilling privacy and legal requirements, and transparently with respect to ethical concerns. In the specific domain of Medical Imaging, in this paper we sketch a research plan devoted to the definition and implementation of query languages that can unambiguously express semantically rich queries on possibly multi-dimensional images, in a human-readable, expert-friendly and concise way. Our approach is based on querying images using Topological Spatial Logics, building upon a novel spatial model checker called VoxLogicA, to execute such queries in a fully automated way.Source: MEDI 2021 - Advances in Model and Data Engineering in the Digitalization Era, pp. 285–301, Tallinn, Estonia, 21-23/06/2021
DOI: 10.1007/978-3-030-87657-9_22
Metrics:
Belmonte G., Broccia G., Bussi L., Ciancia V., Latella D., Massink M.
Nowadays a plethora of health data is available for clinical and research usage. Such existing datasets can be augmented through artificial-intelligence-based methods by automatic, personalised annotations and recommendations. This huge amount of data lends itself to new usage scenarios outside the boundaries where it was created; just to give some examples: to aggregate data sources in order to make research work more relevant; to incorporate a diversity of datasets in training of Machine Learning algorithms; to support expert decisions in telemedicine. In such a context, there is a growing need for a paradigm shift towards means to interrogate medical databases in a semantically meaningful way, fulfilling privacy and legal requirements, and transparently with respect to ethical concerns. In the specific domain of Medical Imaging, in this paper we sketch a research plan devoted to the definition and implementation of query languages that can unambiguously express semantically rich queries on possibly multi-dimensional images, in a human-readable, expert-friendly and concise way. Our approach is based on querying images using Topological Spatial Logics, building upon a novel spatial model checker called VoxLogicA, to execute such queries in a fully automated way.Source: MEDI 2021 - Advances in Model and Data Engineering in the Digitalization Era, pp. 285–301, Tallinn, Estonia, 21-23/06/2021
DOI: 10.1007/978-3-030-87657-9_22
Metrics:
See at:
ISTI Repository | link.springer.com | link.springer.com | CNR ExploRA